\chapter{FLWAnalizer}
\section{Necesidades de usuario}
Como se ha mencionado a lo largo de este proyecto surge la necesidad de poder expresar y definir restricciones sobre los procesos de negocios para de manera declarativa y fundamentalmente asistir al usuario a realizar tal fin. La existencia de diferentes tecnologías hace quizás una tarea ardua al momento de querer describir procesos complejos y someterlos a las propiedades antes mencionadas. \emph{FLWA} intenta solucionar este problema logrando la unión de estas tecnologías y proporcionar el resultado antes descripto aportando procesos escenciales para la comunicaciones entre las diferentes herramientas y asistencia al usuario final por medio de un entorno gráfico.\\
\\\newline
\emph{FLWA} permitirá tomar un modelo definido por medio de la herramienta \emph{YAWL} y poder aplicarle diferentes tipos propiedades o restricciones deseables para luego poder verificarlas de una manera automática y sencilla para el usuario. De esta manera sería útil realizar estas funcionalidades mediante una interfaz gráfica, permitiendo al usuario definir sus propias restricciones, editando los modelos visuales ayudado con herramientas y facilitando la definición nuevas propiedades mediante el uso de plantillas permitiendo reusarlas cuando lo desee. Por último realizar todas estas características tanto la construcción de las propiedades y de la verificación de las mismas para finalmente visualizar los resultados de las propiedades verificadas.
\\\newline
En la siguiente sección se darán detalles de todas las características que presenta la herramienta desarrollada \emph{FLWA}.
 
\section{Características}
A continuación se describen cada una de las funcionalidades de \emph{FLWA} las cuales asistirán al usuario.

\subsection{Modelos YAWL}
En esta sección se describe una de todas las funcionalidades que mas tiempo llevo en el desarrollo. Estos modelos son definidos en primera instancia por la herramienta \textit{YAWL} que hemos descripto anteriormente en el capítulo 3.\\
\emph{FLWA}, mediante la opción de abrir un archivo, permite elegir un modelo creado por \textit{YAWL} e visualizarlo de manera gráfica para su análisis como se mencionó anteriormente. La figura 4.1 es resultado de abrir con \emph{FLWA} el mismo modelo que tratamos en el capítulo 3 \textit{SimpleMakeTripProcess.yawl} en la que se puede apreciar las tareas o \textit{Task}, el nombre de las mismas, las condiciones(en este caso particular las condiciones de Input y output únicamente) y las relaciones entre ellos. 

\begin{figure}[h!]
\centering
\includegraphics[scale=0.7]{images/simpleMakeTripProcessFLWA.png}
\caption{Vista del modelo YAWL SimpleMakeTripProcess.yawl mediante \emph{FLWA}}
\end{figure}

Para la visualización de compuertas, como se muestra en la figura 4.2, además de su representación gráfica como parte del modelo acompañando a una tarea, \emph{FLWA} presenta un panel, a modo de botones, donde aclara para cada compuerta seleccionada su definición. Esto es, si es una compuerta de distribución (\textit{SPLIT}) o de sincronización (\textit{JOIN}) y, en cada caso, su tipo: AND, OR, XOR. Este modo de visualizar las compuertas respeta la forma en la cual se visualizan en la herramienta \textit{YALW}.

\begin{figure}[h!]
\centering
\includegraphics[scale=0.7]{images/simpleMakeTripProcessFLWA1.png}
\caption{SimpleMakeTripProcess.yawl con \emph{FLWA}}
\end{figure}

Adicionalmente \emph{FLWA} permite la edición del modelo deseado en cuanto al control de posición, es decir, permite cambiar la posición en la que se encuentra ya sea una tarea, una condición o incluso los elementos de imput y output.
Además de todo la descripción gráfica del modelo y de la edición de los elementos del mismo, esta herramienta permite representar de manera muy similar a como lo realiza YAWL la visualización de las regiones de cancelación. Esta característica está dada de la siguiente manera; si una tarea posee la propiedad de cancelar una región, ésta estará diferenciadas de las que no mediante un punto de color rojo. Si se quisiera conocer que región es cancelante solo es necesario seleccionar la tarea ésta y se verá en el modelo aquellas tareas en rojo, definiendo la región de cancelación.

\begin{figure}[htb]
\centering
\includegraphics[scale=0.9]{images/cancelationPlace.png}
\caption{Región de cancelación en \emph{FLWA}}
\end{figure}

En la figura 4.3 se presenta un escenario en el cual se visualiza la tarea (time out) como una tarea cancelante y en delineados con rojo las tareas y condiciones que ésta cancela. En esta imagen podemos ver que se aplica ``doble-click'' sobre la tarea \textit{Time Out} se dibujará todo un conjunto de tareas y condiciones describiendo cual es la región de cancelación. La tarea \textit{Preare Trans Quote} también tiene la propiedad de producir una región cancelante.\\

\begin{figure}[htb]
\centering
\includegraphics[scale=0.6]{images/flwaTabs.png}
\caption{Región de cancelación en \emph{FLWA}}
\end{figure}

Adicionalmente \emph{FLWA} permite interpretar modelos en los cuales se tiene tareas compuestas o \textit{Composite Task} las cuales como se describió en el capítulo 2 pueden contener un submodelo con las mismas características que el modelo principal. Siendo éste el caso \emph{FLWA} respeta la forma de visualización adoptada por \emph{YAWL} mediante pestañas o \textit{Tabs} consiguiendo así acceder a todos los modelos de una manera rápida y sencilla. En la figura 4.4 se muestra como ejemplo un escenario en el cual para cara tarea compuesta de la red principal "Overall" una pestaña que contiene la subred que detalla el comportamiento de cada una de éstas.\newpage


se toma nuevamente como ejemplo a \textit{Orderfulfilment} ya que éste posee la complejidad necesaria para mostrar el resultado de tomar modelos con tareas múltiples mediante \emph{FLWA}.


\subsection{Definición de Fluentes sobre \textit{Workflows}}
Como se mencionó anteriormente sería muy bueno poder definir los fluentes sobre los procesos de negocio para facilitar la definición de propiedades que acarrean mayor complejidad. \emph{FLWA} permite hacer esto, es decir si ya se tiene un modelo de \emph{YAWL} interpretado en \emph{FLWA} se puede crear tantos fluentes como sea necesario. Estos fluentes como se describió en el capítulo 2 posee condiciones en las cuales este fluente se ``prende'' y otras en las que se``apagan''. Por otra parte, a cada tarea presente en el modelo se le puede asociar dos eventos \textit{start} y \textit{end}. Estos eventos no permitirán describir el comportamiento en la tarea, es decir modelar el intervalo desde que el flujo ingresa a la tarea hasta que se desprende de ella.


Como se detallará en la próxima sección, el análisis de los modelos de \textit{workflows} se llevará a cabo mediante la definición y posterior verificación de propiedades temporales. Como se introdujo en la sección 2.3, contar con fluentes en la definición de propiedades nos brindan la posiblidad de capturar estados abstractos de nuestro modelo. El valor de verdad de estos estados abstractos (fluentes) están determinados por la ocurrencia de eventos del modelo, en particular en caso de modelos de \textit{workflows}, sus valores se definen en término de eventos de comienzo y finalización de tareas asociadas a dicho modelo. Para facilitar la definición de fluentes, es decir, la creación de los mismos y la especificación de los eventos que los caracteriza, \emph{FLWA} provee una forma visual de hacerlo mediante la selección de los eventos de activación (que lo vuelven verdadero) y desactivación (lo tornan falso) en la representación gráfica del modelo.

Estos fluentes luego pueden  incorporarse en la definición de propiedades a verificar brindando la posibilidad de capturar de manera flexible diferentes situaciones del modelo.

\begin{figure}[h!]
\centering
\includegraphics[scale=0.6]{images/fluentUses1.png}
\caption{\textit{Usos de fluentes en FLWA}}
\end{figure}

En la figura 4.5 podemos ver que se han definido dos elementos \textit{fluent A} y \textit{fluent B}. Se puede ver que se encuentra seleccionado el \textit{fluent A} y que éste cuenta con dos eventos configurados, los eventos \textit{register.start} y \textit{pay.end}. Esto quiere de decir que el fluente A se ``encenderá'' en \textit{register.start} y se ``apagará'' en \textit{pay.end}.\\\newline
En la figura 4.6 se tiene seleccionado el fluente B pero esta vez éste cuenta con los eventos \textit{register.start} y \textit{bookcar.end}. Nuevamente, el fluente B se activará en el evento \textit{register.start} se desactivará en \textit{bookcar.end}.\\

\begin{figure}[h!]
\centering
\includegraphics[scale=0.6]{images/fluentUses2.png}
\caption{\textit{Usos de fluentes en FLWA}}
\end{figure}

Cada fluente que se crea se agrega como un directorio raíz en en apartado de \textit{fluents}, luego cada evento que se vaya agregando a un fluente será fácilmente ubicado en subdirectorio del fluente elegido. De esta manera todos los eventos en los cuales activa el fluente se ubicarán en el directorio \textit{Turn On} y en \textit{Turn Off} los que desactiven el fluente. Todos estos directorios y subdirectorios se pueden expandir o encojer.\\\newline 
Además de lo descripto anteriormente en ambas imágenes se puede visualizar la presencia diferentes cursores, cada uno de ellos tiene una función en particular que se detalla a continuación.
\begin{itemize}
\item\textbf{Cursor selección:} Este cursor se describe como un puntero normal, con la propiedad de poder seleccionar y editar la visualización del modelo. Además se podrá visualizar las compuertas de la tarea selecciona y las regiones de cancelación; en caso de éstas últimas la acción responde a un ``double-click''.
\item\textbf{Cursor On} Este tipo de cursor se representa como el anterior pero además presente un punto de color verde. Éste es útil para poder definir en que eventos en los que el fluente seleccionado se verá activado.
\item\textbf{Cursor Off} El cursor Off es similar al anterior pero en lugar de tener un punto de color verde es rojo. Y se utiliza con el mismo propósito pero para seleccionar en que tareas se va desactivar el fluente seleccionado.
\item\textbf{Cursor Borrador}Éste último cursor se puedo ver una flecha de punta mas pequeña y con una imagen de goma de borrar. Tiene la funcionalidad de borrar cualquier evento seleccionado.
\end{itemize}

Además de lo comentado sobre los cursores, se brinda la posibilidad de sustituir un evento por el opuesto, es decir reemplazar un evento en donde por ejemplo el \textit{fluente A} se activa por un evento en donde A se desactiva.
En el menú superior se encuentra la funciones de crear fluentes o de suprimirlos se se lo desea.\\\newline

Otras de las características que presenta la definición de fluentes es la de destacar de una manera visual aquellas \textit{Tabs} o pestañas cuyo modelo tiene asociado al menos un fluente, esto se puede apreciar con mas detalle en los modelos YAWL los cuales poseen tareas compuesta generando así submodelos que serán representados en otras \textit{Tabs}. \\
En la siguiente figura 4.6 se detalla la funcionalides antes mencionada mediante una imagen encima de la pestaña en la cual se definen fluentes sobre ella, se puede ver fácilmente que tanto \textit{Ordering} como \textit{Carrier\_Appointment} poseen algún evento del fluente A. O dicho de otra manera el fluente A solo define eventos en  \textit{Ordering} y\textit{Carrier\_Appointment}.

\begin{figure}[h!]
\centering
\includegraphics[scale=0.6]{images/signOnTabs.png}
\caption{\textit{Definición de fluentes en modelos compuestos}}
\end{figure}

Esta característica solo describe la posibilidad de poder definir \textit{workflows} sobre los modelos \emph{YAWL} pero no se  el uso de estos fluentes. En la sección siguiente se detalla la definición de propiedades para estos modelos y el uso de los fluentes definidos.

\newpage
\subsection{Definición de Propiedades}
Como uno de los objetivos principales de este trabajo es la definición de propiedades sobre modelos \textit{YAWL}, para ofrecer esto al usuario, \emph{FLWA} implementa un editor sencillo con la inclusión de los operadores lógicos y el manejo de la información del modelo bajo análisis, mediante el cual se pueden definir las propiedades deseadas. Este editor permite la definición, eliminación y modificación de las propiedades que se necesiten.\\

El panel de propiedades de \textit{FLWA} cuenta con dos partes; las propiedades en el panel central y el panel de operadores que se encuentra en el lado izquierdo del panel anterior. El panel de operadores cuenta con los operadores de la lógica de primer orden y los operadores temporales. Estos operadores, pueden escribirse dentro de cada propiedad o bien al aplicarles una acción de \textit{drag-and-drop} sobre un cuadro de texto, dibujan en el mismo el operador seleccionado y dependiendo de si éste es binario o unario, se insertarán además los paréntesis para los correspondientes operadores.\\ Por otra parte, los operandos se obtienen al seleccionar los espacios concedidos por el operador. De esta manera se consigue una segunda ventana de menor tamaño conteniendo todas las tareas del modelo, las cuales se le podrá asociar el tipo de evento, es decir \textit{start} o \textit{end}. Por otro lado, para incorporar fluentes definidos previamente como variables proposicionaes de una fórmula, se pueden arrastrar desde la lista de fluentes hasta la correspondiente posición dentro de la formula mediante \textit{drag-and-drop}. La figura 4.8 refleja un ejemplo de la definición de dos propiedades, con operandos que han sido tomados del modelo como lo son  \textit{Ordering} y \textit{Freight in Transit}. Cada propiedad definida posee un selector (checkbox) que puede utilizarse para indicar cuáles propiedades va a estar afectadas para su verificación o eliminación.

\begin{figure}[h!]
\centering
\includegraphics[scale=0.7]{images/proprertiesUses.png}
\caption{\textit{Definición de propiedades sobre modelos \textit{FLWA}}}
\end{figure}

Como alternativa a la definición de propiedades de la manera que se describió anteriormente FLWA provee por otra parte un módulo mediante el cual se podrá utilizar unas plantillas o \textit{templates} para la definición de propiedades. Estas plantillas o patrones de propiedades permiten al usuario disponer de una serie de propiedades generalmente utilizadas sin la necesidad de especificar su correspondiente fórmula en \textit{LTL}. Cada plantilla está compuesta por su descripción en lenguaje natural, su correspondiente fórmula y una descripción gráfica siguiendo el lenguaje gráfico establecido en DECLARE. La fórmula de cada propiedad permanece oculta pero dependiendo de ésta se le solicita al usuario que ingrese determinados parámetros (en general los operandos) para lograr la construcción de la misma. Cada parámetro podrá instanciarse con eventos del modelo o con fluentes, de la misma manera como se detalló con anterioridad.\\
Una vez que se haya completado la formula, ésta se puede agregar a las otras que ya han sido definidas. La imagen 4.9 muestra una situación que resulta de seleccionar una de las plantillas definidas, en este caso \textit{exactly1}, asegurando que dicho evento sucede exactamente una sola vez. La construcción de la propiedad está dada mediante la selección del evento \textit{register\_3.start} que posteriormente será agregada al resto de las propiedades definidas sobre el modelo.\\\newline

\begin{figure}[h!]
\centering
\includegraphics[scale=0.5]{images/templateExactly1.png}
\caption{\textit{Plantilla exacttly1 de \textit{FLWA}}}
\end{figure}

En la figura 4.10 se muestra otro tipo de plantilla \textit{Responded Existence} la cual expresa la siguiente restricción, si el evento A ocurre al menos una vez entonces el evento B si ocurre, debe hacerlo antes que el evento A. Para este caso disponemos de un fluente definido sobre el modelo y cómo este fluente también puede utilizarse como variable proposicional de algunos de los parámetros que posee la propiedad definida. Los eventos elegidos serán \textit{pay\_11.end} como parámetro A y el fluente definido \textit{A} como parámetro B de la plantilla.


\newpage
\begin{figure}[h!]
\centering
\includegraphics[scale=0.6]{images/templateRespondedExistence.png}
\caption{\textit{Plantilla Responded Existence de \textit{FLWA}}}
\end{figure}

Como comentamos anteriormente existe un número variado de plantillas, que se pueden aplicar en numerosas situaciones y su uso dependerá del modelo que se esté tratando. Estas plantillas están almacenadas en un documento de texto cuya información se ``leerá'' al momento de solicitar el modulo de \textit{templates}. Esto a la posibilidad a que si el usuario desea eliminar, modificar o incluso agregar nuevas plantillas lo podrá hacer sin ningún problema, modificando el archivo de configuración de \emph{FLWA}. En caso de que se desee agregar una plantilla nueva sólo bastará agregar al final del archivo la información correspondiente como se muestra a continuación (ya instanciado para la propiedad \textit{existence2}).\\


\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=xml,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={template,id,text,display,description,numberBranch,name,image},
}

\lstinputlisting[caption=Templates]{codes/teplateExample.xml}
A Continuación se describen las propiedades necesarias para la definición de plantillas.
\begin{itemize}
\item\textbf{Id:} Esta propiedad define un número que representará univocamente a un templete. Es decir no debería haber dos templates con el mismo id.
\item\textbf{Description:} Aquí se especifica en lenguaje formal o no, lo que va a realizar la propiedad a definir.
\item\textbf{Display:} Esta etiqueta representa un texto que defina el comportamiento de la plantilla. 
\item\textbf{Name:} Nombre de la propiedad.
\item\textbf{Text:} Este campo es el mas importante, al igual que el anterior, puesto que aquí debería definirse la formula. Hay que notar que ciertos operadores no están soportados con codificación UTF-8, por lo tanto hay que realizar una conversión previa.
\item\textbf{Number of Branch:} Esta propiedad representa en número de parámetros que serán necesarios para la construcción de la formula.
\item\textbf{Image:} Se puede colocar(es opcional) una imagen que represente a la propiedad. La ubicación de la imagen debe ser absoluta es decir debe incluirse la ubicación desde la raíz.

\end{itemize}


\subsection{Verificación de Propiedades}
Una vez que se tienen todas las propiedades definidas y los fluentes configurados con sus correspondientes eventos del modelo, se procede a la verificación de estas formulas mediante el uso de la herramienta \emph{LTSA}. Cabe recordar que para la verificación se utiliza la herramienta \emph{LTSA}, esta integración es oculta para el usuario final.\\
La verificación consta de seleccionar primero las propiedades que se pretende verificar y luego aplicar la función de \textit{Check Property} de las opciones inferiores. En una nueva pantalla de opciones particulares se debe seleccionar sobre qué red del modelo se quiere realizar la verificación, esta opción brinda la posibilidad de poder realizar verificaciónes locales a un sub-workflow (aquel definido como detalle de una tarea compuesta) cuando sea pertinente. En caso de propiedades globales del modelo, el usuario debe seleccioar el proceso (red) principal del mismo. Una vez seleccionado el contexto de verificación, se presiona sobre el nombre de la propiedad para iniciar su verificación.

\begin{figure}[h!]
\centering
\includegraphics[scale=0.6]{images/propertyVerification.png}
\caption{\textit{Verificación de propiedades en \textit{FLWA}}}
\end{figure}

En esta figura se puede ver que se han definido solo dos propiedades y que según cada proceso, en este caso \textit{LESS\_TAHN\_TRUCK\_LOAD}, se realiza una verificación del mismo modo que lo realiza \emph{LTSA}. En caso de que se encuentre una contradicción al final del resultado arrojado por FLWA se encontrará un indicación que la propiedad fue violada. Por ejemplo si la primer propiedad es invalidad, se obtendría la etiqueta \textit{Trace to property violation in A1}. Por otra parta se podrá, en este caso, visualizar la traza que hace invalida la propiedad verificada. La figura 4.11 permite ver cuando una propiedad es invalidad, la traza representando al contraejemplo de la misma y por último la definición de la misma coloreada en rojo. 

\begin{figure}[h!]
\centering
\includegraphics[scale=0.5]{images/resultPropertyFluentViolated.png}
\caption{\textit{Propiedad invalidad en \textit{FLWA}}}
\end{figure}

Para el caso en que la propiedad es valida, por supuesto no habrá un contra ejemplo pero si se podrá visualizar la definición de la misma coloreada en verde.

\subsection{Características Adicionales}
Otras posibilidades que ofrece \emph{FLWA} es el de realizar una copia de todas las propiedades y fluentes que se hayan definido. Del mismo modo, si se cuenta con una copia de las propiedades y fluentes realizada por \emph{FLWA}, esta se podrá cargar siempre y cuando estas definiciones se han realizado sobre el modelo el cual se las desea aplicar. Esto en otras palabras asegura que siempre que se quiera abrir un archivo con propiedades y fluentes sea efectivo para el modelo corriente.
